$\forall$${\it es}$:ES, ${\it e'}$, $e$, $a$:E. ($e$ $<$loc $a$) \& $a$ $\leq$ ${\it e'}$ $\Rightarrow$ [$e$, ${\it e'}$] $=$ ([$e$, pred($a$)] @ [$a$, ${\it e'}$]) $\in$ E List